(declare-fun var0 () String)
(declare-fun var1 () String)
(declare-fun var2 () String)
(declare-fun var3 () Int)
(declare-fun var4 () Int)
(declare-fun var5 () Int)
(declare-fun var6 () Bool)
(declare-fun var7 () Bool)
(declare-fun var8 () Bool)
(assert (<= (str.len var2) (str.len var1)))
(assert (>= (str.len var0) (str.indexof (str.at "Rb""${#w\\i=" var4) (str.replace var2 """sx8Bc99c#" var2) (str.len var2))))
(assert (> (str.indexof var1 var0 var4) (str.indexof var1 var2 var3)))
(assert (> (str.len var2) (str.len "BYoYtHb/u#")))
(check-sat)
